Problem: first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) from(X) -> cons(X) Proof: Complexity Transformation Processor: strict: first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) from(X) -> cons(X) weak: Matrix Interpretation Processor: dimension: 1 max_matrix: 1 interpretation: [from](x0) = x0 + 1, [cons](x0) = x0, [s](x0) = x0, [nil] = 0, [first](x0, x1) = x0 + x1 + 50, [0] = 64 orientation: first(0(),X) = X + 114 >= 0 = nil() first(s(X),cons(Y)) = X + Y + 50 >= Y = cons(Y) from(X) = X + 1 >= X = cons(X) problem: strict: weak: first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) from(X) -> cons(X) Qed